\begin{tabbing}
$\forall$${\it es}$:ES, $X$:AbsInterface(Top), $e$:E.
\\[0ex]($\uparrow$($e$ $\in_{b}$ prior($X$)))
\\[0ex]$\Rightarrow$ \=((prior($X$)($e$) $<$loc $e$)\+
\\[0ex]\& ($\uparrow$(prior($X$)($e$) $\in_{b}$ $X$))
\\[0ex]\& ($\forall$${\it e''}$:E. (${\it e''}$ $<$loc $e$) $\Rightarrow$ (prior($X$)($e$) $<$loc ${\it e''}$) $\Rightarrow$ ($\neg$($\uparrow$(${\it e''}$ $\in_{b}$ $X$)))))
\-
\end{tabbing}